Aufgabe 1 ist keine Spezifikationsübung, sondern eine Übung in der Semantik.

Heute kommen die Formalen Regeln der Semantik an.

Das ist das einzige, was wir heute auf dem Programm haben.

Diese Regeln werden verwendet, um alle Aufgaben auf dieser Zettel zu lösen.

In Aufgabe 1 geht es um etwas Wohlbekanntes, nämlich den Neutral Exclusion Protokoll.

Für Informatiker ist das wohlbekannt.

Das ist in einer richtigen und falschen Variante.

Man kann solche Protokolle falsch machen.

Ein Anwendungsgebiet ist, dass Protokolle korrekt sind.

Oder dass sie nicht korrekt sind, einschließlich Security-Protokoll.

In diesem Fall nicht viel mit Passwörtern.

Einfach nur gegenseitiger Ausschluss beim Betreten eines kritischen Abschnitts.

Man sieht hier den User-Prozess.

Der hat einen kritischen Abschnitt, in dem man nichts macht, außer wieder rein und wieder rauszugehen.

Das ist das Enter und Exit, das wir in der Mitte sehen.

Er setzt eine Semaphore, bevor er reingeht.

Er akquiriert die, wie man so schön sagt.

Und lässt sie wieder frei, nachdem er wieder rausgegangen ist.

Im fehlerhaften Protokoll lässt er die Semaphore wieder frei, bevor er rausgeht.

Da soll man die Semantik ausrechnen für jeweils über die beiden Grunddefinitionen, User und Semaphore.

Mutex 1 ist natürlich ein bisschen trivial.

Weil es da nichts auszuschließen gibt.

Es gibt keinen konkurrierenden Prozess, sondern nur einen Benutzerprozess.

Damit man sieht, wie das Elementar funktioniert mit dieser Kommunikation zwischen User-Prozess und Semaphore.

Wichtig dabei ist, dass der Zugang zur Semaphore nach außen versteckt wird.

Das beeinflusst die Übergänge, die in diesem Prozess stattfinden können.

Man sollte vielleicht auch mal einen Kommentar verlieren, auch wenn das nicht hier steht, was das bewirkt.

Das könnte man direkt als Frage zufügen.

Was würde eigentlich passieren, wenn man die nicht verstecken würde?

P&V?

Ist schon klar, haben wir hier taktisch auch durchexerziert.

Dann kommt der Ernstfall.

Das ist Mutex 2, wo es einen konkurrierenden Prozess gibt, der ebenfalls in den kritischen Abschnitt will.

Da soll ebenfalls die Semantik ausgerechnet werden.

Nachdem man das gemacht hat, soll man argumentieren, weil ich nicht formal formuliert habe, was das Mutex Problem gelöst wird.

Da soll man anhand der Formalen Semantik, die man unter 2. aufgeschrieben hat, sagen, warum das Mutex Problem gelöst wird.

Dann kommt das Ganze noch mal auf einen zu.

Dann wird der User austauschen und noch mal die Semantik ausrechnen und dann feststellen, dass das Mutex Problem nicht gelöst wird.

Das ist also einfach eine eher triviale Übung, diese Semantik auszurechnen, damit man diese Regeln mal ins Gefühl kriegt.

Die Sie ja noch gar nicht kennen, kommen gleich.

Aufgabe 2 ist, was das hier praktisch schon diskutiert.

Das kann einmal formal durchgewiesen werden, dass wir per Augenschein in der Lage sind, Parallelität eigentlich rauszukodieren.

Das mit dem Rauscodieren kommt als Aufgabe 3.

Hier sehen wir jedenfalls, dass man mit mittels Parallelität, mit relativ kurzen Ausdrücken, relativ große LTS darstellen kann.

Konkret soll hier eben gesagt werden, wie groß das LTS, was da erzeugt wird, eigentlich ist.

Relativ klar, was da als Lösung hinkommt.

Das soll dann bewiesen werden, per Induktion, einfach mal als Übung in Induktion und gleichzeitiger Anwendung von diesen Semantikregeln und Induktion, dass das dann auch wirklich eine korrekte Formel ist.

Dass es auch nicht so rasend schwer geht, deswegen nur 5 Punkte.

Dann kommt Aufgabe 3. Die hat zwei Teile, die nicht so richtig schwer sind.

Teil 1, das klingt zwar abenteuerlich, man soll zu einem gegebenen LTS eine Prozessdefinition aufschreiben, die gerade dieses LTS beschreibt.